Notes taken by Jason Schuchardt
Homework
Further reading
- Proofs and Types, Jean-Yves Girard (1989)
- Lecture Notes on the Lambda Calculus, Peter Selinger (2013)
- Syntax and Semantics of Dependent Types, Martin Hofmann (1997)
- Intuitionistic Type Theory, Per Martin-Löf (1980)
- Homotopy Type Theory, The Univalent Foundations Program (2013)
- Univalent foundations and the equivalence principle, Benedikt Ahrens, Paige Randall North (2019)
- Univalent categories and the Rezk completion, Benedikt Ahrens, Chris Kapulkin, Michael Shulman (2014)
Other resources
- The HoTT list. A Google Group intended for experts. Interesting developments and events are often announced here.
- The HoTT Cafe. A Google Group intended for non-experts.
- A wiki on the nLab.
- A calendar. There are usually a few week-long schools for students each year.